Nuprl Lemma : choicef_wf
2,24
postcript
pdf
xm
:XM,
T
:Type,
P
:(
T
Prop). (
a
:
T
.
P
(
a
))
(
x
:
T
.
P
(
x
))
T
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
Prop
,
t
T
,
x
:
T
.
P
(
x
)
,
XM
,
Dec(
P
)
,
P
Q
,
A
,
False
Lemmas
not
wf
,
xmiddle
wf
origin
xm:XM, T:Type, P:(T
Prop). (
a:T. P(a)) 
(
x:T. P(x)) T xm:XM, T:Type, P:(TProp). (a:T. P(a)) (x:T. P(x)) T x:A. B(x) Qx:A. B(x) Tx:T. P(x)
Q
A